﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Collections.ObjectModel;

namespace OpSatPlan.Encoder
{
    public class OperatorDrillDownEncoder
    {
        private CnfEncoder mEncoder;
        private Dictionary<string, string> mClauses;
        public OperatorDrillDownEncoder(CnfEncoder encoder)
        {
            this.mEncoder = encoder;
            this.mClauses = new Dictionary<string, string>();
        }
        public void Encode(IEnumerable<Operator> operators)
        {
            foreach (Operator op in operators)
            {
                this.mClauses.Clear();
                this.Encode(op, operators);
            }
            this.mClauses.Clear();
        }
        private void Encode(Operator op, IEnumerable<Operator> operators)
        {
            foreach (Action a in op.Actions)
            {
                this.DrillDown(a, op, operators, 0);
            }
        }
        private void DrillDown(Action action, Operator op, IEnumerable<Operator> operators, int drill)
        {
            ClauseTemplate clause;
            Identifier id;

            clause = new ClauseTemplate(this.mEncoder);
            clause.Add(op, false);
            for (int i = 0; i <= drill; i++)
            {
                id = action.Identifiers[i];
                // this is anded together with the operator value, therefore it is negated.
                clause.Add(id.AtomicFormula, (id.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), !id.Value);

                // encode the sub identifiers
                if (i != drill || drill + 1 == action.Identifiers.Count)
                {
                    foreach (Identifier sub in id.SubIdentifiers)
                    {
                        clause.Add(sub.AtomicFormula, (sub.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), !sub.Value);
                    }
                }
            }
            
            if (drill + 1 == action.Identifiers.Count)
            {
                // encode the rest of pre and effs
                this.WriteClauses(clause, action, action.Preconditions, true, IdentifierTypes.Precondition);
                this.WriteClauses(clause, action, action.AddEffects, true, IdentifierTypes.Effect);
                this.WriteClauses(clause, action, action.DeleteEffects, false, IdentifierTypes.Effect);                
            }
            else
            {
                if (this.mClauses.ContainsKey(clause.GenerateClause(0)))
                {
                    this.DrillDown(action, op, operators, drill + 1);
                    return;
                }
                else
                    this.mClauses.Add(clause.GenerateClause(0), clause.GenerateClause(0));

                
                id = action.Identifiers[drill];

                // the operator was true but it may not have affected this truth change
                clause.Add(id.AtomicFormula, (id.IdentifierType == IdentifierTypes.Precondition ? 1 : 0), id.Value);

                // find all actions with the identifiers the same as the current drill down.
                List<Identifier> ids = new List<Identifier>();
                for (int i = 0; i <= drill; i++)
                {
                    ids.Add(action.Identifiers[i]);
                }
                var res = from oper in operators
                          from act in oper.Actions
                          where ids.All(k => act.ContainsIdentifier(k)) 
                          select act;

                id = action.Identifiers[drill + 1];

                foreach (Action a in res)
                {
                    Identifier idTemp = null;
                    var idRes = from x in (from ik in a.Identifiers
                             where ik.IdentifierType == id.IdentifierType &&
                                    ik.Value == id.Value &&
                                    ik.AtomicFormula.Definition == id.AtomicFormula.Definition
                             select ik)
                             where x != null
                             select x;
                    if (idRes != null && idRes.Count() > 0)
                    {
						foreach(Identifier ik in idRes)
						{
							if(id.AtomicFormula.Arguments.All(o => ik.AtomicFormula.Arguments[id.AtomicFormula.Arguments.IndexOf(o)].Type == o.Type))
							{
                       			idTemp  = ik;
                    			break;
							}
						}
					}
                    else
                    {
                        var idRes2 = from x in
                                         (from ik in a.Identifiers
                                          where ik.IdentifierType == id.IdentifierType &&
                                                 ik.Value == id.Value &&
                                                 ik.AtomicFormula.Arguments.Any(o => id.AtomicFormula.Arguments.Contains(o))
                                          select ik)
                                     where x != null
                                     select x;
                        if (idRes2 != null && idRes2.Count() > 0)
                        {
                            idTemp = (Identifier)idRes2.ElementAt(0);
                        }
                    }
                    if (idTemp != null)
                    {
                        clause.Add(idTemp.AtomicFormula, (idTemp.IdentifierType == IdentifierTypes.Precondition ? 0 : 1), idTemp.Value);
                    }
                }
                this.mEncoder.WriteClauses(clause);
                this.DrillDown(action, op, operators, drill + 1);
            }
        }
        private void WriteClauses(ClauseTemplate clause, Action action, ReadOnlyCollection<AtomicFormula> afs, 
                                    bool value, IdentifierTypes type)
        {
            ClauseTemplate tmpClause;
            var idRes = from id in action.Identifiers
                        where id.IdentifierType == type && id.Value == value
                        select id;
            IEnumerable<AtomicFormula> set;
            if (idRes.Count() == 0)
                set = afs;
            else
            {
                set = from x in (from af in afs
                      where idRes.All(tid => af != tid.AtomicFormula)
                      select af)
                          where x != null
                      select x;
            }
            foreach (AtomicFormula af in set)
            {
                tmpClause = new ClauseTemplate(clause);
                tmpClause.Add(af, (type == IdentifierTypes.Precondition ? 0 : 1), value);
                this.mEncoder.WriteClauses(tmpClause);
            }

        }
    }
}
